.skip 4
.center;L'UNIFICATION AU SERVICE DE LA COMPREHENSION
.center;D'ENONCES D'UN LANGAGE DE PROGRAMMATION
.skip 3
.center;Rapport de stage
.skip 1
.center;Daniel GOOSSENS
.center;Departement d'Informatique
.center;Universite Paris VI
.center;JUSSIEU
.center;aout 1978
.skip 4
1. INTRODUCTION.
.skip 2
##L'unification (ROBINSON 1965)
 joue un grand role dans la plupart des programmes
d'intelligence artificielle. En effet, elle permet une grande economie dans
le developpement exponentiel des recherches lors de preuves de theoremes.
Or, il semble qu'il n'y ait pas de limite  a l'extension des algorithmes 
d'unification, et chaque extension represente une nouvelle economie dans
l'explosion des recherches. Ainsi, si les deux expressions P(Q(a,b),a)
et P(y,Q(x,y)) ne sont pas unifiables selon ROBINSON, elles le sont par
un algorithme qui tiendrait compte de l'eventuelle propriete de commutativite
de P et Q.
.break
##Cependant, les extensions actuelles (STICKEL 1975, KUHNER 1977, PLOTKIN 1972)
consistent a
definir les algorithmes d'unification a partir de certaines proprietes
des fonctions a unifier. Lorsqu'on peut se donner une semantique precise
de ces fonctions (pour le langage LISP par exemple), ces algorithmes
deviennent bien vite insuffisants, car ils ne tiennent pas compte des
proprietes, meme fort simples, autres que celles pour lesquelles ils ont
ete prevus.
.break
##Je propose une notation a base de FILTRES pour construire l'equivalent
d'une semantique axiomatique du langage LISP. Le sens des fonctions
LISP n'est plus represente par un ensemble de relations algebriques,
mais d'une maniere que HEWITT qualifie de CONCEPTUELLE (HEWITT,
YONEZAWA 1976). Ceci permet de decrire completement un grand nombre de
fonctions LISP, sans utiliser de structure de controle iterative ou
recursive, ce qui evite beaucoup de preuves par induction, en les
remplacant par des unifications (une unification donne d'ailleurs
beaucoup plus d'informations qu'une simple preuve de theoreme).            
.break
##Cette notation conceptuelle n'est pas specifique a un domaine
semantique particulier. Dans ce papier, je l'applique au langage
LISP, et je montre qu'on peut en decrire a la fois la partie 
manipulation de listes et la partie arithmetique, ainsi que diverses 
stuctures plus simples, comme par exemple les entrees sorties.
.skip 3
2. L'UNIFICATION SELON ROBINSON.
.skip 2
##Elle permet d'identifier des structures qui ne different que par certains
elements, l'un d'entre eux au moins etant une variable d'element.
.break
Exemples: (x y z sont universellement quantifies)
.skip 1
(EQUAL x y) et (EQUAL (CONS 'a z) (cons 'b z)) sont indentifiables
grace a la substitution:
.break
x = (CONS 'a z)####y = (CONS 'b z)
.skip 1
(EQUAL x x) et (EQUAL (CONS 'a z) (CONS 'b z)) par contre ne sont pas
unifiables.
.skip 1
LIMITATIONS:
.break
##Voici une serie d'exemples intuitivement unifiables mais pour lesquels
l'unification de robinson echoue.
.skip 1
- x et (G x); plutot que la substitution x = (G x), l'unificateur devrait
donner toutes les informations possibles sur x, sachant que c'est un point
fixe de G. Par exemple, si (G x)#=#(CONS a x), alors l'unification 
devrait echouer grace a l'information que l'ensemble des elements LISP
muni de l'operation CONS ne possede pas d'element neutre. Si 
(G x)#=#(APPEND x x), alors l'unificateur devrait ramener la substitution
x#=#().
.skip 1
- (+ x y) et (+ y x); L'unification selon robinson ne tient pas compte
de la propriete de commutativite de l'addition et echoue.
.skip 1
- (APPEND x (APPEND y z)) et (APPEND (APPEND x y) z); de meme (propriete
d'associativite de la fonction APPEND.)
.skip 1
- (APPEND x (APPEND y z)) et (APPEND (APPEND x y) (APPEND x z));
l'unificateur devrait donner la substitution x = () en utilisant ses
informations sur l'associativite de APPEND et son element neutre.
.skip 3
3. L'UNIFICATION DE FONCTIONS.
.skip 2
##Certains travaux (STICKEL 1975, KUHNER MATHIS RAULEFS SIEKMANN 1977,
PLOTKIN 1972)
se sont donnes pour but de construire
pour chaque propriete suffisamment generale (commutativite, associativite,
idempotence) un unificateur.
.skip 1
exemple:(a et b ne sont pas des variables, mais des objets atomiques.
        ils ne peuvent etre decomposes)
.break
- (+ (* a b) a) et (+ y (* x y)); la substitution la plus generale est
x#=#b, y#=#a. Il suffit de tenir compte de la propriete de commutativite
de + et *.
.skip 1
LIMITATIONS:
.break
##Ces unificateurs se revelent cependant bien vite insuffisants lorsqu'ils
sont appliques sur des domaines precis, ou l'on possede une semantique 
intuitive des objets rencontres, semantique basee sur leur utilisation
exhaustive. Voici une serie d'exemples intuitivement unifiables pour
qui connait bien les fonctions LISP utilisees, et pour lesquels les
unificateurs actuels echouent. Ces exemples contiennent les fonctions
CDR, qui admet une liste comme argument et rend cette liste sans son
premier argument si elle n'est pas vide, et la liste vide sinon, 
CAR, qui rend le premier element d'une liste, PLUS, qui additionne
deux entiers,
LENGTH, qui rend le nombre d'elements d'une liste, APPEND, qui concatene
deux listes, et REVERSE, qui rend la liste inverse des elements d'une
liste. AND est une structure de controle qui rend la valeur de son
dernier argument si toutes les valeurs de ses arguments sont differentes
de NIL, et NIL sinon.
.skip 1
1. (LENGTH (APPEND x y)) et (LENGTH (APPEND y x)) s'unifient sans
contrainte.
.skip 1
2. (LENGTH x) et (LENGTH (CDR x)) ne s'unifient que par la substitution
x = ().
.skip 1
3. (LENGTH (APPEND x y)) et (PLUS (LENGTH y) (LENGTH a)) ne s'unifient
que par la substitution (LENGTH x) = (LENGTH a).
.skip 1
4. x et (REVERSE (REVERSE y)) s'unifient par la substitution x = y.
.skip 1
5. (AND x (CAR x)) et (AND x (CAR (APPEND x y))) s'unifient sans
contrainte.
.skip 1
##Ces exemples ressemblent plutot a des theoremes a demontrer qu'a des
expressions a unifier. Pourtant, il est possible de construire un 
processus deterministe d'unification qui resolve ce genre d'exemples
sans evidemment faire appel au demonstrateur de theoreme au service
duquel il serait. Notons l'avantage sur la demonstration de theoremes:
pour l'exemple 3, par exemple, un demonstrateur de theoremes ne 
donnerait que l'information que (LENGTH#(APPEND#x#y))#=#(PLUS#(LENGTH#y)
(LENGTH#a)) n'est pas un theoreme.
.break
C'est un tel processus d'unification qui est decrit ici et dont le
listing est donne en appendice.
.skip 1
##Pour tenir compte de l'exemple 1, il est d'abord possible de construire
l'unificateur de telle sorte qu'il tienne compte d'une propriete comme:
(LENGTH (APPEND x y)) = (PLUS (LENGTH x) (LENGTH y))##A## en esperant
que cette propriete soit suffisamment generale dans le domaine ou
l'on se trouve. Mais si cette propriete rend compte des exemples 1 et 3,
elle ne rend pas compte de l'exemple 2, dont la comprehension est 
pourtant tres aisee. Pour l'exemple 2, l'unificateur devrait tenir
compte de proprietes beaucoup plus particulieres comme:
.break
#z←
/ x = (APPEND z (CDR x)), [(APPEND x y) = y] => [x = ()], 
[x = (CDR x)] => [x = ()]
.skip 2
3.1 Tenir compte d'un large evantail de proprietes.
.skip 1
##La propriete##A## n'englobe pas totalement le sens de LENGTH. On pourrait
substituer a LENGTH une infinite d'autres fonctions dans ##A## sans que 
##A## ne soit faux. Le meme probleme se pose avec la fonction REVERSE et
un grand nombre d'autres fonctions LISP de base.
.skip 1
##Un moyen commode de definir completement une fonction LISP, c'est 
d'utiliser des structures de controle iteratives ou recursives. 
LENGTH serait definie par exemple par: 
.skip 1
.nofill
       (LENGTH ()) = 0
       (LENGTH (CONS x y)) = (ADD1 (LENGTH y))
.fill
.skip 1
##Cependant, lie a ce probleme, il y a celui de l'utilisation de 
proprietes de fonctions par l'unificateur. Pour unifier
(APPEND#x#(APPEND#y#z)) et (APPEND#(APPEND#x#y)#(APPEND#x#z)) ##B##
en utilisant la propriete de commutativite de APPEND, l'unificateur
peut avoir plusieurs choix s'il n'est pas correctement defini. Il
peut utiliser l'equation a la maniere d'un demonstrateur de 
theoremes par exemple, en commencant par remplacer ##B## par
(APPEND#(APPEND#(APPEND#x#y)#x)#z) puis par
(APPEND#(APPEND#x#(APPEND#y#x))#z). D'une maniere generale, le
probleme se pose pour chaque propriete du type a = b dont on
veut que l'unificateur tienne compte: quand remplacer a par b ou
b par a.
.break
##C'est pourquoi chaque ajout d'une propriete oblige a reconcevoir
completement l'unificateur(1).
.footnote 3
------------------------------------------------------------
(1) L'unificateur ne devrait pas faire appel a un demonstrateur
de theoremes.
.end footnote
.skip 1
##Ce second probleme rend plus cruciale la remarque faite lors
du premier probleme, a savoir le besoin constant de proprietes 
plus particulieres les unes que les autres pour tenir compte
de nouveaux cas.
.break
Par ces considerations, la solution qui consiste a utiliser des
structures de controle recursives pour definir des relations 
aussi precises que possibles entre fonctions, rend alors
totalement utopique l'idee de construire un unificateur qui
tiendrait compte de ces definitions. Il faut s'en remettre a un systeme de 
demonstration qui se chargera d'executer symboliquement (KING 1975,
BOYER ELSPASS LEVITT 1975, HEWITT 1975, YONEZAWA 1976,
BALZER GOLDMAN 1977, WERTZ 1978)
et d'induire lorsque c'est necessaire, c'est-a-dire a chaque definition
recursive (BOYER MOORE 1973).
.SKIP 1
##Pour illustrer les problemes que posent cette approche, voici un 
exemple:
.skip 1
.nofill
          [(APPEND L L) = (APPEND M M)] => L = M
.fill
.skip 1
##Ce theoreme pourtant aisement comprehensible, est difficilement demontrable
par induction, principalement du fait que L et M sont doubles. De quelle
propriete de APPEND l'unificateur doit-il tenir compte pour ramener comme
resultat de l'unification de (APPEND L L) et (APPEND M M) la substitution
L = M ? Du present chapitre, il nous faut conclure que l'unificateur
a besoin de definitions completes, mais ne faisant pas appel a des
structures de controle recursives ou iteratives, des fonctions
qu'il manipule. C'est l'objet des representations conceptuelles qui
permettent de representer un grand nombre de fonctions LISP de base,
notamment toutes celles rencontrees jusqu'a present (appendice).
.skip 3
4. RESULTAT D'UNE UNIFICATION.
.SKIP 2
##Peu de travaux se sont interesses au resultat a obtenir d'une 
unification.
Le probleme peut, evidemment, egalement se reecrire: quels sont les
buts de l'unification ? quels travaux peut-on, ou ne peut-on pas,
demander a un unificateur ? Quelle information un unificateur
doit-il fournir, ou plus precisement, sous quelle forme ?
.break
##Le precedent chapitre repond partiellement a ces questions.
Voici quelques exemples destines a jeter un peu de confusion
quant a la reponse:
.skip 1
- (CDR x) et (CDR y) il ne s'agit pas ici de ramener x = y. 
en fait, la reponse (CDR x) = (CDR y) est suffisante. Le
resultat n'a plus la forme "variable = expression", mais
"expression = expression".
.skip 1
- (NTH z x) et (NTH z y) la reponse (NTH z x) = (NTH z y) est 
suffisante.
.skip 1
- (NTH z x) et (NTH y x) par contre, ici, la reponse z = y
s'impose.
.skip 1
##On pourrait, a partir de ces exemples, etudier un relation
"partie de", savoir la reconnaitre, et ne pas unifier deux
expressions dont la valeur est une partie d'une des variables. 
Puis on pourrait etudier un grand nombre d'autres relations
reliees a d'autres classes de fonctions LISP. C'est pourtant 
a mon avis une approche qui a souvent trompe en intelligence artificielle.
La suite le montrera, ou l'on est capable de resoudre la plupart
de ces problemes par une approche uniforme, c'est a dire sans jamais
se polariser sur une quelconque de ces notions particulieres
de "partie de", "allonger", "raccourcir", "contenir", "structurer",
"decouper", "longueur", "milieu", "debut", "fin", qui touchent
a certains processus et elements LISP.
.break
Dernier exemple:
.skip 1
- (LENGTH x) et (LENGTH y) la reponse est (LENGTH x) = (LENGTH y).
cependant, si y = (APPEND x x), le resultat doit etre x = ().
.skip 2
##La simple reponse vrai ou faux a la question E1 et E2 sont-ils
unifiables n'est pas suffisante. L'ensemble de couples d'elements
associes que constitue une substitution est une information tres
utile. L'unification de (APPEND A B) et (APPEND C D) devrait
ramener les substitutions:
.skip 1
.nofill
        C = (APPEND A C2)    |  D = (APPEND D1 B)
        B = (APPEND C2 D)    |  A = (APPEND C D1)    1
.fill
.skip 1
En effet, comprendre le programme:
.skip 1
.nofill
        (DE FOO (X Y N)
            (IF X
                   (FOO (CDRNTH N (APPEND Y X)) Y N)
                   NIL))
.fill
.skip 1
c'est entre autres considerer les deux cas ou la valeur de 
(CDRNTH#N#(APPEND#Y#X))
est plus grande ou plus petite que la valeur de X
pour distinguer les cas ou la fonction FOO est indefinie, des autres.
Or, comprendre (CDRNTH A B), c'est voir B sous la forme (APPEND B1 B2)
ou (LENGTH B1) = A. Si B = (APPEND Y X), il faut unifier
(APPEND B1 B2) ET (APPEND Y X).
.skip 2
##D'une maniere generale, l'unificateur doit ramener toutes les
substitutions possibles. Cependant, A = C et B = D, A = D et
C = B = (), sont des substitutions possibles pour ##1##. Dans
un but qui n'est pas seulement un but d'economie, l'unificateur
doit ramener un nombre minimum de substitutions dont la reunion
englobe toutes les substitutions possibles et qui sont deux a deux
disjointes(1).
.footnote 10
------------------------------------------------------------
(1) L'union ou l'intersection de deux substitutions sont
definies en appendice, dans le cadre du present unificateur.
D'autre part, le fait que la variable C2 soit soulignee dans
##1## prend a present un sens: Pour que les deux substitutions
soient disjointes, il faut par exemple que C2 soit different
de (), sans quoi on a des deux cotes l'instanciation C = A et B = D.
.end footnote
.skip 3
5. UNIFICATION DE REPRESENTATIONS CONCEPTUELLES.
.skip 2
##Les representation conceptuelles (HEWITT YONEZAWA 1976) que
j'utilise semblent basees au depart sur une connaissance empirique
des langages de manipulation de listes mais je discuterai au
paragraphe 7 un certain nombre de proprietes formelles qui les
privilegient.
.skip 1
##Ces representations conceptuelles sont des ensembles de regles
qui sont elles-meme des couples de filtres. Un filtre est 
defini par la grammaire:
.skip 1
.nofill
   <filtre>:= cste | variable | (<filtre> <liste-de-filtres>)
   <liste-de-filtres>:= <filtre> <liste-de-filtres> | ←∧
.fill
.skip 1
ou cste peut etre n'importe quelle constante LISP
(les signes speciaux "!", "?", "}", et " L " doivent cependant
etre quotes pour eviter toute confusion)
 et ou variable
peut etre d'un des 4 types suivants:
.skip 1
- !(domaine nom)
.left margin 5
C'est une variable d'element, qui peut coincider, par simple
filtrage (HUET 1976), avec n'importe quel element LISP du 
domaine. Le domaine est l'union d'un nombre quelconque des
domaines de base: nombres, litteraux, {NIL⎇, listes non vides.
La liste de ces domaines de base peut evidemment etre etendue.
le nom individualise la variable.
Lorsque le domaine est l'ensemble des elements lisp, l'ecriture
est abbreviee a !nom.
.left margin 0
.skip 1
- ?nom
.left margin 5
C'est une variable de sequence qui peut coincider avec n'importe
quelle sequence d'elements LISP, sauf la sequence vide lorsque
le nom est souligne.
La definition de la fonction CAR pourrait s'ecrire:
.skip 1
.nofill
     (CAR ()) = ()    (CAR (!1 ?2)) = !1
.fill
.skip 1
.left margin 0
- (L  <liste-de-filtres>)
.left margin 5
Cette variable coincide avec n'importe quelle liste de la forme
(?e  ?e  ... ?e ) ou (<liste-de-filtres>) coincide avec chaque
(?e ). La definition de la fonction LENGTH pourrait etre:
.skip 1
.nofill
     (LENGTH ((L   !x ))) = n
.fill
.skip 1
Il faut noter que l'indice i dans !x# fait partie du nom. chaque
variable de la sequence est ainsi individualisee.
.skip 1
.left margin 0
- (} <filtre1> <filtre2>)
.left margin 5
Cette variable coincide avec n'importe quel element e tel que <filtre2>
coincide avec e mais pas <filtre1>. La definition de la fonction EQUAL
pourrait etre:
.skip 1
.nofill
     (EQUAL !1 !1) = T   (EQUAL !1 (} !1 !2)) = NIL
.fill
.left margin 0
.skip 2
##Voici, pour illustrer l'efficacite de cette notation conceptuelle,
les exemples precedemment non resolus. L'unificateur sera decrit en detail
au chapitre suivant.
.skip 1
- x et (CONS y x)
.left margin 5
Les representations conceptuelles de x et (CONS y x) sont
respectivement (?x) et (!y ?x). L'unification de ces deux
filtres echoue par la seule regle qui empeche une variable
(de filtre) D'etre associee a un filtre qui la contient.
.left margin 0
.skip 1
- (APPEND x (APPEND y z)) et (APPEND (APPEND x y)(APPEND x z))
.left margin 5
les representations conceptuelles de ces deux expressions sont
respectivement (?x ?y ?z) et (?x ?y ?x ?z). L'unification de ces
deux filtres donne (?x) = ().
Il faut egalement noter qu'une quelconque composition des
fonctions APPEND a partir de la deuxieme expression par exemple,
aurait la meme representation conceptuelle.
.left margin 0
.skip 1
- (LENGTH (APPEND x y)) et (LENGTH (APPEND y x))
.left margin 5
Les deux representations conceptuelles sont n+m et m+n, ou
x#=#((L##!1#)) et y#=#((L##!2#)), ce qui s'unifie sans
contrainte.
.left margin 0
.skip 1
- (LENGTH x) et (LENGTH (CDR x))
.left margin 5
La representation conceptuelle de (CDR x) conduit a deux cas:
x = () (CDR x) = (), et x = (!1 ?2) (CDR x) = (?2).
Dans le second cas, les deux representations conceptuelles sont
1+n et n, ce qui ne s'unifie pas, et dans le premier cas, elles
sont 0 et 0. Le resultat de cette unification est donc x = ().
.left margin 0
.skip 1
- (LENGTH (APPEND x y)) et (PLUS (LENGTH y) (LENGTH z))
.left margin 5
Les deux representations conceptuelles sont n+m et m+p, ou
x#=#((L##!1#)) y#=#((L##!2#)) et z#=#((L##!3#)), ce qui
s'unifie par la substitution n = p.
.left margin 0
.skip 1
- x et (REVERSE (REVERSE y))
.left margin 5
les deux representations sont !x et (?y), ou x = !x et y = (?y).
Ce qui s'unifie avec !x = (?y). Notons qu'en plus de l'information
x = y, l'unificateur reduit le domaine de y pour que REVERSE soit
definie.
.left margin 0
.skip 1
- (AND x (CAR x)) et (AND x (CAR (APPEND x y)))
.left margin 5
Les deux representations sont !1 et !1 si x = (!1 ?2), ou bien
NIL et NIL si x = (). Dans les deux cas, l'unification se fait sans
contrainte.
.left margin 0
.skip 1
- (APPEND x x) et (APPEND y y)
.left margin 5
les deux representations conceptuelles correspondantes sont
(?x ?x) et (?y ?y), ou x#=#(?x) et y#=#(?y),
 ce qui s'unifie par la substitution
?x#=#?y.
.left margin 0
.skip 1
- (NTH z x) et (NTH y x)
.left margin 5
.skip 1
si NTH n'est definie que lorsque z ou y contiennent un nombre 
inferieur ou egal a la longueur de x, alors les deux
representations conceptuelles sont (?3) et (?3), ou
x#=#((L##!1#)#?3). Le resultat de l'unification est
n#=#m, ou y = n et z = m. Dans les exemples presentes
en appendice, NTH est definie dans le cas ou son premier
argument est un nombre plus grand que la longueur de son
second. dans ce cas, la valeur est le second argument 
tout entier.
.left margin 0
.skip 1
- (APPEND a b) et (APPEND c d)
.left margin 5
les deux representations sont (?a ?b) et (?c ?d), ou a = (?a)
b = (?b), c#=#(?c) et d#=#(?d). l'unification de ces deux
representations donne deux substitutions (et ce, simplement
parceque leur union ne peut etre codee en filtres):
.break
?c#=#?a#?c2########?d#=#?d1#?b
?b#=#?c2#?d########?a#=#?c#?d1
.left margin 0
.page
6. LE PROCESSUS DE META-FILTRAGE.
.skip 2
6.1 Filtrage et Meta-filtrage.
.skip 2
##Le processus de META-FILTRAGE est en relation avec un processus plus
simple de FILTRAGE (HUET 1976, GREUSSAY 1978).
si le processus de filtrage peut etre considere comme l'operation consistant
a verifier si une expression (donnee) possede une propriete (filtre), le
processus de meta-filtrage peut etre considere comme l'operation consistant
a trouver quel sous-ensemble d'un ensemble infini de donnees contient
toutes celles qui possedent une propriete representee par un filtre, d'ou
la relation META. C'est en fait la meme relation qu'entre le processus 
d'evaluation, qui consiste a appliquer une fonction sur une donnee, et
le processus de meta-evaluation qui est cense representer l'equivalent
d'une infinite d'evaluations.
.skip 1
##Dans la pratique, l'ensemble infini de donnees est egalement represente
par un filtre et le processus de meta-filtrage peut etre considere
comme une operation commutative d'unification de filtres (cette operation
sera notee "<::>")
.skip 2
6.2 Resultat du meta-filtrage de deux filtres.
.skip 2
##Le resultat du meta-filtrage de deux filtres F1 et F2 est un ensemble
de couples de listes d'associations. Chaque couple est une substitution
qui permet d'unifier F1 et F2 par un simple processus de propagation
des associations (paragraphe 6.9). Chaque couple contient une premiere
liste d'associations de la forme: (v = F) ou v est une variable
de F1 et F une portion de F2, ou bien de la forme: 
(sequence-de-variables#=#sequence-de-filtres) ou sequence-de-variables
est une sequence de longueur indefinie de variables de type "!" ou "?",
et sequence-de-filtres une sequence de longueur indefinie de filtres.
La seconde liste d'associations contient les variables associees de F2.
Cette division est evidemment ambigue lorsqu'une meme variable se retrouve
dans F1 et F2. Je n'en tiendrai pas compte dans les exemples qui suivent.
Dans le cas ou le meta-filtrage echoue, la valeur est NIL.
.break
##Chaque fois qu'une association est operee, toute occurence de la variable
associee dans le reste des filtres a comparer et dans les listes
d'associations deja construites, est remplacee par ce a quoi elle a ete
associee. Le processus ne peut boucler grace a une propriete d'acyclicite
des associations qui est soigneusement preservee lors de leurs construction
et modifications (voir detail du processus de meta-filtrage, paragraphes
6.3, 6.4, 6.5).
.skip 2
6.3 Variables de type "!".
.skip 2
##Lorsque les filtres ne contiennent que des constantes ou des variables
de type "!" (variables d'element), le processus de meta-filtrage est
proche de celui d'unification.
.break
exemple:
.skip 1
- (!x (a !y)) <::> ((!z b) !x) donne:
.break
########!x = (a b), !y = b, !z = a
.skip 2
} Une variable ne peut etre associee a un filtre
.left margin 2
qui la contient.
.skip 1
.left margin 0
} Lorsqu'une variable peut etre associee a un filtre,
.left margin 2
un test est opere sur le filtre pour s'assurer qu'il est compatible
avec le domaine de la variable. Ce test tres simple est construit
a partir des predicats LISP de base: ATOM, NUMBP, NULL, et
d'une operation d'intersection pour le cas ou deux variables doivent
etre associees. Dans ce cas, cette operation calcule l'intersection
des deux domaines.
.break
exemples:
.skip 1
- !atom <::> !list####donne: 
.break
##########!atom = (), !list = ()
.break
Le domaine de !atom est l'ensemble des atomes et celui de !list
l'ensemble des listes y compris la liste vide.
.skip 1
- !atom <::> !nb####donne:
.break
##########!atom = !nb1, !nb = !nb1
.break
Les domaines de !nb et !nb1 sont l'ensemble des entiers.
.skip 1
- !nb <::> !list####echoue.
.left margin 0
.skip 2
6.4 Variables de type "?"
.skip 2
##Le processus de meta-filtrage admet deux filtres comme arguments
et les parcourt ensemble de gauche a droite. Il ne peut alors
rencontrer que les cas suivants (les variables definies au debut
du paragraphe 6 sont utilisees comme meta-symboles pour decrire
des classes de filtres. Lorsqu'elles sont utilisees en tant
que telles, elles sont quotees par ").
.skip 1
situation generale: ("?"!nom ?1) <::> (?2)
.break
sous cas:
.skip 1
- ("?"!nom ?1) <::> ("?"!nom ?2)
.break
.left margin 2
Le processus est poursuivi (appel recursif) avec les 2 arguments
(?1) et (?2).
.left margin 0
.skip 1
- ("?"!nom ?1) <::> ()
.break
##Le processus echoue.
.skip 1
- ("?"!nom) <::> (?2 "?"!nom ?3)
.break
.left margin 2
Appel recursif avec les deux arguments () et (?2 ?3).
.left margin 0
.skip 1
- ("?"!nom) <::> (!e1 !e2 ...!en)
.break
.left margin 2
Echoue si l'un des !ei contient "?"!nom. Sinon, l'association
"?"!nom#=#!e1#!e2#...#!en est ramenee (acyclicite).
.left margin 0
.skip 1
- sinon
.break
.left margin 2
"?"!nom est associee a une portion de (?2). i:e (?2) est considere
comme la concatenation de deux filtres; (?2)#=#(?3#?4).
.skip 1
} "?"!nom est associe a ?3.
.break
} Cette association est transmise sur (?1) et (?4), donnant (?1)' et
(?4)', et sur la liste d'associations courante.
.break
} Elle est ajoutee a la liste d'associations courantes.
.break
} La valeur ramenee est celle de l'appel recursif avec les deux
arguments (?1)' et (?4)' et la nouvelle liste d'associations.
.break
} Le processus est applique pour toutes les valeurs possibles
de ?3 et de ?4. Le processus de meta-filtrage fait ainsi appel a une
STREAM-FONCTION (HEWITT 1974) qui a chaque appel allonge la
portion denotee ici par (?3).
.left margin 0
.skip 2
6.4.1 La stream-fonction
.skip 2
##La stream-fonction se charge de fournir a une variable en position de
demandeur une partie de filtre. Le filtre etant de la forme 
(!e1#!e2#...#!en), la stream-fonction ne peut fournir qu'une partie
du type (!e1#!e2#...!ei) avec i <= n. Le decoupage du filtre se fait en
fonction des !ei rencontres.
.break
##La stream-fonction discrimine d'abord entre deux types d'!ei 
differents: les elements (constantes et variables d'element) et
les sequences (variables de sequence).
.skip 1
- Si tous les !ei sont des elements, la stream-fonction fournit
tour a tour les portions suivantes:
.skip 1
.nofill
  ()
  (!e1)
  (!e1 !e2)
   .
   .
   .
  (!e1 !e2 ... !en)
.fill
.skip 1
- Apres chaque appel, la stream-fonction conserve la portion fournie:
(!e1#!e2#...#!ei), et a chaque nouvel appel, decoupe un nouveau morceau
de (!ei+1#!ei+2#...#!en), et l'ajoute a (!e1#...!ei). Si !ei+1 est une 
variable de sequence, deux cas sont a considerer suivant que cette
variable est suivie
.break
1- d'un element ou de rien
.break
2- d'une variable de sequence
.break
Si !ei+1 est une variable de type "?", dans le premier cas, cette variable
est scindee en deux variables de type "?", la premiere etant ajoutee
a (!e1#...!ei) et la seconde a (!ei+1#...#!en). A l'appel suivant
de la stream-fonction, la variable primitive est reconstituee et 
ajoutee toute entiere a (!e1#...#!ei).
Dans le second cas, elle est scindee en deux variables de type "?",
le domaine de la seconde etant restreint a l'ensemble des listes
non vides. Ceci permet, lorsque plusieurs substitutions sont
ramenees, de n'avoir que des substitutions disjointes.
.skip 1
- Chaque fois qu'un des !ei est "absorbe" par la stream-fonction,
c'est-a-dire chaque fois qu'un element est rajoute a la portion a
fournir, ou qu'une variable de sequence est reconstituee et
rajoutee, l'element !ei+1 est teste. Si c'est une variable de
sequence, elle est scindee par le processus decrit ci-dessus
et la portion gauche est ajoutee a la partie a fournir.
.skip 1
- Chaque fois qu'une variable de sequence est "absorbee",
la stream-fonction est immediatement reactivee. 
.skip 1
- Appliquee sur une liste vide, la stream-fonction ne fournit
pas de valeur.
.break
Tous ces cas particuliers ont le but de reduire au maximum le
nombre de solutions a l'unification de deux filtres tout en livrant
un ensemble complet de solutions.
.skip 1
- Si !ei+1 est une variable de type " L ", les memes cas particuliers
s'appliquent. La seule difference est la scission en deux variables.
i:e si !ei+1#=# ("L"##!a1#!a2#...!ap), l'entier !m est scinde en
!m#=#!x+1+!y. Alors,
 !ei+1#=#("L"##!a1#!a2#...!ap)#!a1#...!ap#("L"##!a1#...!ap).
("L"##!a1#...!ap) est ajoute a (!e1#...!ei), le reste a (!ei+1#...!en)
et le processus entier est reapplique. Si par exemple !a1 est une 
variable de sequence, elle est immediatement scindee. Lorsque !ap est
atteint, la variable est reconstituee, puis rajoutee a (!e1#..!ei),
comme pour les variables de type "?".
.skip 1
exemple:
.skip 1
Si le filtre est:
.break
########(?1 a ?2 ?3 b ?4)
.break
la stream-fonction fournit tour a tour les portions suivantes:
.skip 1
.nofill
   (?5)               (avec (?1) = (?5 ?6))
   (?1 a ?6)          (avec (?2) = (?6 ?7))
   (?1 a ?2 ?8)       (avec (?3) = (?8 ?9))
   (?1 a ?2 ?3 b ?10) (avec (?4) = (?10 ?11))
.fill
.skip 2
6.5 Variables de type " L ".
.skip 2
##Les memes cas que pour les variables de type "?" sont a
distinguer. La difference principale touche au cas:
.skip 1
- (("L"##?F)) <::> (!e !e1 ... !ep)
.left margin 2
Si !e est une variable de sequence et que p est different de zero,
la valeur est un appel recursif avec les deux arguments inverses.
Ainsi, !e se trouvera en position de demandeur et la stream-fonction
se chargera de decouper ("L"##?F). Ceci permet de se limiter aux 
sous-cas suivants:
.break
- (("L"##?F)) <::> (!e)
.break
ou !e est une variable de sequence. Si !e est du type "?", la valeur
est un appel recursif avec les deux arguments inverses. Si 
!e#=#("L"##?G), le meta-filtreur ne s'occupe que du cas ou 
(?F)#=#(!X1#...!Xa) et (?G)#=#(!Y1#...!Yb). ou tous les !Xi et !Yi sont
des elements.
.break
} Si a = b, le meta-filtreur est rappele avec les deux arguments !n et !m,
puis avec les deux arguments (?F) et (?G), mais dans un contexte ou
l'on conserve l'information sur la course des curseurs !i et !j 
i:e#!i#et#!j#de#1#a#!n. 
.break
} Sinon, il calcule les plus petits entiers c et d tels que a*c = b*d,
puis se rappelle avec les arguments !n et (!v1#!v2#...!vc) puis 
!m et (!w1#...!wd) ou les !vi sont des variables numeriques
(voir paragraphe 6.7) identiques, ainsi que les !wi. Il se rappelle
enfin avec les deux arguments:
.break
####("L"##?F1#...?Fc) et ("L"##?G1#...?Gd)
.break
- (("L"##?F)) <::> (!e1#...!en)
.break
ou !e1 est un element. La valeur est un appel recursif avec les
deux arguments:
.break
####(?Fi/1 ("L"##?F)) et (!e1#...!en)
.break
(?Fi/1 est la sequence ?F ou toutes les occurences du curseur !i
sont remplacees par 1)
.break
ce processus peut boucler, par exemple dans un cas comme:
.break
####(("L"##?F)) <::> (!a1 ... !ap ("L"##?G))
.break
suivant les longueurs de (?F), (?G) et (!a1#...!ap).
.left margin 0
.skip 1
##Lorsque le meta-filtreur compare deux filtres dans un contexte contenant
des courses de curseurs, chaque occurence d'un curseur provoque un
comportement particulier. Comparer "!Xf(i)" et "!Yg(i)" dans le contexte
i#de#1#a#!n, c'est en fait comparer ("!Xf(1)"#..."!Xf(n)") et
("!Yg(1)"#..."!Yg(n)"). Si X#=#Y par exemple, il s'agit de prevoir
certains cas particuliers, pour preserver la propriete d'acyclicite
des associations, qui, seule, garantit la terminaison du processus de
propagation. Cette partie du meta-filtreur, n'etant que partiellement
implementee, n'est pas developpe ici.
.skip 2
6.6 Variables identiques
.skip 2
##Si l'on applique directement le processus decrit ci-dessus a
l'exemple suivant (les variables ne sont plus utilisees comme
meta-symboles)
.skip 1
- (?1 a) <::> (a ?1)
.break
Alors on n'obtient pas de resultat. En effet, ?1 est en position de 
demandeur. Le filtre () lui est d'abord fourni. (?1)#=#() est une
solution retenue. Ensuite, ?1, dans le second filtre, est divise en
deux variables de sequence: ?1#=#?2#?3. La partie (a#?2) est fournie
au ?1 demandeur. Il s'agit alors d'unifier (?2#?3) et (a#?2). La
meme chose se produira lorsqu'il s'agira de scinder ?2. En fait,
ce processus genere une infinite d'unifieurs:
.break
(?1)#=#(), (?1)#=#(a), (?1)#=#(a#a), ...
.break
Or, l'unifieur general peut etre represente par un seul filtre:
.break
(?1) = ((L##a))
.break
##D'une maniere generale, il s'agit de detecter les cas suivants:
(les variables sont a nouveau utilisees comme meta-sybmboles pour
decrire des classes de filtres)
.break
(!x ?y) <::> (?z !x) et (?z !x) <::> (!x ?y)
.break
ou !x est une variable de sequence.
.break
Dans ce cas, il faut comparer (?y) et (?z), mais d'une maniere
differente
.break
Au probleme: "Le probleme de l'unification de deux filtres peut-il
se ramener a celui de l'unification d'un filtre quelconque et
d'un autre filtre particulier ?" la reponse est oui.
Le filtre particulier est "(!a#!a)". Unifier deux filtres
!P et !Q, c'est unifier "(!a#!a)" et (!P#!Q). Le probleme
n'est pas plus simplifie pour autant.
.break
Dans le cas qui nous occupe, il faudrait unifier le filtre
particulier "((?1#?2)(?2#?1))" et ((?y)(?z)), ce qui ne
simplifie pas non plus le probleme. La solution est
alors (!x)#=#"((L##(?1#?2)) ?1)".
.break
Dans un cas particulier comme:
.skip 1
- "(a b a b ?1)" <::> "(?1 b a b a)"
.break
.left margin 2
ceci permet de ramener les deux solutions:
.break
"(?1)"#=#"((L##a b a b) a)"
.break
"(?1)"#=#"((L##a b a b) a b a)"
.break
Une solution plus sophistiquee consiste a ne pas utiliser le
filtre particulier "((?1#?2)(?2#?1))" mais
"(((L##?1#?2))((L##?2#?1)))", ce qui permet de ne ramener, pour
l'exemple present, qu'une seule solution:
.break
"(?1)"#=#"((L##a b) a)"
.break
.left margin 0
Ce processus echoue cependant toujours dans le cas particulier:
.break
- "(?x ?y)" <::> "(?y ?x)"
.break
ou la solution est:
.break
"?x"#=#"(L##?z)"
"?y"#=#"(L##?z)"
.skip 2
6.7 Variables numeriques.
.skip 2
##Une classe d'entiers positifs peut etre representee par un filtre
de la forme:
.break
####("NB" !e1 ... !en)
.break
ou chaque !ei est soit le symbole "1", soit une variable de sequence.
Si !ei#=#("L"##?F), alors ("NB" ?F) doit decrire une classe d'entiers.
!ei denote alors la multiplication de !n par ("NB" ?F).
.break
Par exemple, "(NB ?x ?x)" decrit la classe des entiers positifs
pairs et "(NB ?x ?x 1)" la classe des entiers positifs impairs.
.break
- L'addition de deux entiers ("NB" ?n) et ("NB" ?m) est representee
par ("NB"#?n#?m).
.break
- La soustraction de ces deux entiers consiste a unifier ("NB"#?n)
avec ("NB"#?m#"?R"). Le resultat est "?R" (ou plus precisement,
ce a quoi il a ete associe).
.break
##La propriete de commutativite de l'addition est construite dans
le processus de meta-filtrage. Dans le cas:
.break
######("NB" !e ?f) <::> ("NB" ?G1 !e ?G2)
.break
la valeur est un appel recursif avec les deux arguments:
.break
######("NB" ?f) et ("NB" ?G1 ?G2)
.skip 2
6.8 Une amelioration puissante du processus de meta-filtrage.
.skip 2
##Voici un cas interessant:
.break
- "(?1 ?1)" <::> "(?2 ?2)"
.break
.left margin 2
Si l'on applique le processus decrit, il faut scinder "?2" en
deux variables "?3" et "?4", fournir la premiere a "?1", puis
meta-filtrer "(?3)" et "(?4 ?3 ?4)", ce qui echoue. Il faut
alors scinder "?2" en deux variables "?3" et "?4", fournir
a "?1" le filtre "(?3 ?4 ?3)", et meta-filtrer "(?3#?4#?3)"
et "(?4)", ce qui donne "(?3)"="()". D'ou la solution
"?1"#=#"?4" et "?2"#=#"?4". Le processus est encore plus
complexe dans le cas:
.break
- "(?1 ?1 ?1)" <::> "(?2 ?2 ?2)"
.break
Or, il y a moyen de simplifier ce processus dans un grand nombre de cas 
equivalents. Cette amelioration consiste a construire  la longueur 
abstraite de deux filtres du type (!e1#...!en) que l'on veut meta-filtrer,
et a meta-filtrer ces deux longueurs abstraites. Construire la longueur
abstraite, c'est remplacer chaque !ei par le symbole "1" si c'est un
element, le laisser tel quel si c'est une variable de type "?", et
si c'est une variable de type ("L"##?F), le remplacer par
("L"##?G) ou (?G) est la longueur abstraite de (?F). Les longueurs
abstraites representant des classes d'entiers, la propriete de commutativite
joue et permet beaucoup de simplifications.
.break
Dans le cas:
.break
"(?1 ?1 ?1)" <::> "(?2 ?2 ?2)"
.break
on calcule d'abord "(NB ?1 ?1 ?1)"#<::>#"(?2#?2?#2)", ce qui livre
l'information "?1"#=#"?2".i:e les deux sequences ?1 et ?2 ont meme
longueur. La stream-fonction doit alors etre modifiee pour tenir
compte de ce genre d'information.
.break
autre exemple:
.break
- ("?1" ?2) <::> (?3 "?1" ?4)
.break
La comparaison des longueurs abstraites livre l'information que
(?2) et (?3 ?4) doivent avoir meme longueur.
.left margin 2
.skip 2
6.9 Le processus de propagation des associations.
.skip 2
- toute occurence d'une variable de type "!" ou "?" est 
remplacee par ce a quoi elle a ete associee.
.skip 1
- La propagation de !n = (!e1 ... !ea) sur (("L"##?F)) donne
(("L"##?F)("L"##?Fi/i+!e1)#...("L"##?Fi/i+!e1+!e2...+!ea)).
Les expressions de la forme ("L"##?F) sont remplacees par ?Fi/1.
(l'ecriture ?Fi/!x represente la sequence ?F ou toute occurence
de !i est remplacee par !x)
.skip 1
- Propagee sur (("L"##?F1#"!xi"#?F2)) par exemple, une 
association comme "!xj"#=#!G,#j#de#1#a#!n, donne:
(("L"##?F1#!G#?F2)).
7. LES REPRESENTATIONS CONCEPTUELLES ET LE PROCESSUS
###D'UNIFICATION.
.SKIP 2
##Le concept de representation conceptuelle englobe plus que les
filtres ici presentes. De meme, le concept d'unification de
representations conceptuelles englobe plus que le processus de
meta-filtrage. Il est certain que le pouvoir expressif des 
representations conceptuelles est bien moindre que celui
des representations algebriques (GUTTAG 1976 et 1977, ZILLES 1976).
.break
A ce probleme, il faut repondre par deux points:
.skip 1
- Les representations conceptuelles n'empechent pas les 
representations algebriques. Un exemple en est une 
extension du langage CAN (GOOSSENS 1978a), qui permet de
decrire n'importe quel programme LISP. Des exemples sont 
donnes en appendice ou sont decrites, grace a cette extension,
certaines structures de controle du langage LISP.
.skip 1
- Les representations conceptuelles sont plus appropriees au processus
de comprehension que les representations algebriques. La raison en est
que les representations conceptuelles peuvent etre unifiees alors
qu'on ne peut en general que prouver des theoremes au sujet des
representations algebriques. Or, une unification donne plus
d'informations qu'une preuve de theoreme.
.break
De plus, lorsqu'on fait reposer le processus de comprehension
sur la preuve de theoreme, il arrive souvent que pour comprendre une structure,
il faille prouver un theoreme a son sujet et que pour construire ce
theoreme, il faille auparavant comprendre la structure (GOOSSENS 1978b).
.skip 2
##Pour augmenter le pouvoir descriptif des representations conceptuelles,
il faut sans cesse creer de nouveaux types de variables. Le probleme est
que chaque fois qu'un nouveau type de variable est cree, il faut 
modifier completement l'unificateur pour qu'il en tienne compte.
C'est par exemple ce qui arriverait si l'on voulait decrire, en
plus des nombres, des literaux et des listes LISP, des ensembles
d'elements LISP.
.break
##Ces considerations soulevent un probleme tres important: Il
s'agit de savoir comment un systeme pourrait lui-meme definir
de nouveaux types de variables, et changer un processus d'unification
en consequence.
.skip 2
7.1 Canonicite des representations conceptuelles.
.skip 2
##Dans un langage comme LISP, il est facile de coder une meme fonction,
meme simple, de plusieurs manieres differentes. Il est egalement
facile de decrire un ensemble (definir un predicat) de multiples
facons. C'est probablement la reduction importante des possibilites
de decrire un concept, qui confere aux representations conceptuelles
la possibilite d'etre unifiees par un processus relativement peu
complique. Si, au lieu de comparer deux representations par
l'equivalent du predicat LISP EQUAL (identite syntaxique), on le
fait par le processus de meta-filtrage, alors il est fort
probable qu'on puisse parler, pour une classe importante de 
filtres, de representations canoniques des ensembles qu'ils 
denotent (1).
.footnote 6
------------------------------------------------------------
(1) Dans la pratique, il faut ajouter au processus de meta-filtrage
un processus simple de typage des filtres, processus qui, par exemple,
transformerait (!1 ?2) et (?3 !4) en la meme chose, ainsi qu'un
processus d'union de filtres, qui transformerait (!1#?2) et () en (?3).
.end footnote
.skip 1
##A la base de ces considerations, il y a entre autres les exemples
tres convaincants que sont les definitions a base de filtres de
quelques 50 fonctions LISP donnees en appendice. L'utilisation
d'une regle sans appel recursif permet de travailler independamment
sur la forme requise des arguments (filtre gauche) et sur le
resultat de la fonction representee par la regle (filtre droit), ce
que ne permet plus une definition recursive, et tout en
conservant les relations entre donnees et resultats.
.skip 1
##C'est cette propriete de canonicite (2) seule qui doit 
differencier entre representations conceptuelles et autres.
.footnote 3
.skip 1
(2) Cette propriete sous-entend une semantique mathematique des
filtres (qui est esquissee en appendice).
.end footnote
.skip 3
8. UNION ET INTERSECTION DE FILTRES.
.skip 2
##Une semantique tres simple des representations conceptuelles
peut etre esquissee. A chaque filtre F on associe l'ensemble
des elements LISP E tels que (MATCH F E) reussisse (ou MATCH
est un algorithme de filtrage (pattern matching) qu'il 
convient de choisir en fonction des demonstrations que l'on veut menuer a bien.
L'union ou l'intersection de deux filtres est un filtre auquel est associe
l'ensemble union ou intersection des ensembles associes a ces deux 
filtres.
.break
L'union ou l'intersection de deux substitutions se construisent
normalement, excepte pour le cas ou l'on a deux couples de la forme:
.skip 1
.nofill
            x = filtre1   x = filtre2
    
dans le cas de l'union, ceci est remplace par:
   
            x = union de filtre1 et filtre2
  
dans le cas de l'intersection:
   
            x = intersection de filtre1 et filtre2
   
.fill
Le filtre intersection de deux filtres peut aisement etre 
construit par les operations suivantes:
.skip 1
- Unification des deux filtres, ce qui ramene une substitution S.
.skip 1
- Propagation de S sur l'un des deux filtres. Le resultat est le
filtre escompte. Dans le cas ou plusieurs substitutions sont
ramenees, plusieurs filtres sont construits. C'est l'union de
ces filtres qu'il faut considerer.
.page
x
9. BIBLIOGRAPHIE.
.skip 2
.nojustify
.nofill
BALZER, GOLDMAN ←& WILE (1977)
                 "Meta-evaluation as a tool for program
                  understanding"
                  5th IJCAI, MIT Cambridge, August 1977
BOYER, ELSPASS ←& LEVITT (1975)
                 "SELECT--A formal system for testing and
                  debugging programs by symbolic execution"
                  Int. Conf. on Reliable Software,
                  April 1975, pp. 234-245.
CHAILLOUX (1976)  "VLISP-10 manuel de reference"
                  Dept. d'informatique, Univ. PARIS 8, RT 17-76.
GOOSSENS (1978a)  "A system for visual-like understanding of
                  LISP programs"
                  A.I.S.B. Conf. Hamburg, July 1978.
GOOSSENS (1978b)  "Comprehension visuelle de programmes                     
          	  controlee par meta-filtrage"
 		  Groplan: Bulletin de l'AFCET,
		  Groupe Programmation et langages,
                  a paraitre.
GREEN ←& BARSTOW (1975)
                 "A hypothetical dialogue exhibiting a
                  knowledge base for a program understanding
                  system"
                  Stanford A.I. Lab. MA 258, Cpt Science Dept.
                  Report n. Stancs-75-476.
GREUSSAY (1977)   "Contribution a la definition interpretative et 
                  a l'implementation des lambda-langages"
                  These, Universite PARIS 8.
GUTTAG (1976)     
                 "Abstract data types and the development of
		  data structures"
		  Comm. of the ACM, vol 20, no 6, pp 396-404.
GUTTAG (1977)    "The design of data type specifications"
		  2nd Int. Conf. on Soft. Engineering.
		  San-francisco, oct 1976.
HEWITT ←& SMITH (1974)
                 "A plasma primer"
                  A.I. Lab. MIT oct. 74.
HEWITT ←& SMITH (1975)
                 "Towards a programming apprentice"
                  IEEE Trans. on soft. engineering,
                  Vol. SE-1. pp. 26-45.
HUET (1976)
                  "Resolution d'equations dans les langages
		  d'ordre 1, 2, ..., w"
		  These d'etat, Univ. PARIS VII, sept 1976.
.fill
.page
.nofill
IGARASHI, LONDON ←& LUCKHAM (1975)
                  "Automatic program verification I: A logical
                  basis and its implementation"
                  Acta Informatica, Vol. 4, pp. 145-182.
KING (1975)       "A new approach to program testing"
                  Int. Conf. on reliable software,
                  April 1975, pp. 228-233.
KUHNER MATHIS RAULEFS SIEKMAN (1977)
                  "Unification of idempotent functions"
                  5th ijcai, MIT Cambridge, aug 1977.
PLOTKIN G. D. (1972)
                  "Building-in equational theories"
                  Machine Intelligence 7,
                  d. Mitchie (ed.), American elsevier,
		  New-york, 1972.
RICH ←& SCHROBE (1975)
                  "Understanding LISP programs: Towards a
                  programming apprentice"
                  Master's Thesis, EECS M.I.T.
ROBINSON J. A. (1965)
                  "A machine oriented logic based on the
                  resolution principle"
                  J.A.C.M. 12, pp 23-41.
STICKEL (1975)
                  "A complete unification algorithm
       		  for associative-commutative functions"
		  4th ijcai, Tbilisi Georgia USSR.
                  sept. 1975.
WERTZ (1978)      "Un systeme de comprehension, d'amelioration,
                  et de correction de programmes incorrects"
                  These de 3ieme cycle, Univ P. et M. CURIE.
YONEZAWA ←& HEWITT (1976)
                  "Symbolic evaluation using conceptual 
                  representations for programs with 
                  side-effects"
                  M.I.T., A.I. Lab., AI-Memo 399.
ZILLES LISKOV (1975)
                  "Specifications techniques for data
		   abstractions"
		   Proceedings of ACM Int. Conf. on
		   Reliable Software, Los-angeles.
.fill
.page
APPENDICE 1
.skip 3
UNE APPLICATION DE L'UNIFICATION DE REPRESENTATIONS CONCEPTUELLES:
UN META-INTERPRETE DU LANGAGE LISP.
.skip 2
##Voici des exemples d'un systeme de comprehension d'enonces
LISP. Ce systeme, appele CAN (GOOSSENS 1978), traduit le
maximum de ce qu'il lit en representations conceptuelles. Il 
peut etre vu comme un meta-evaluateur du langage LISP. Il
doit en tous cas etre considere comme un simple outil pour
la comprehension des enonces (Il est a mon avis un outil
indispensable pour les systemes plus ambitieux mais
actuellement peu performants de comprehension de
programmes (GREEN BARSTOW 1975, IGARASHI LONDON LUCKHAM 1975,
RICH SHROBE 1975, WERTZ 1978)). Il ne resoud pas, par
exemple, le probleme de savoir quand il faut comprendre ou
quand il n'en est pas besoin.
.skip 1
##Comme le processus de meta-filtrage, il est ecrit en VLISP-10
(CHAILLOUX 1976)
.skip 1
notes: l'ecriture (L##F) se retrouve sous la forme:
(LL<i#n>#F). !xi s'ecrit !x<i+>. !xi+a+1 s'ecrit
!x<i+a+1>. (} x y) s'ecrit (%c% x y).
.page
.skip 4
LECTURE DES RESULTATS:
.skip 2
##A chaque "?" suit une commande LISP classique, qui sera meta-interpretee
au lieu d'etre seulement interpretee. La valeur de la meta-interpretation
suit l'indication "valeur:". Les impressions intermediaires livrent une
trace du processus.
.skip 1
##L'application d'une fonction F sur une liste d'arguments deja evalues
provoque les impressions suivantes:
.skip 1
(F a1 a2 ... an)
.break
;a1 a2 ... an sont les arguments non evalues;
.nofill
X1 = v1
X2 = v2
   .
   .
   .
Xm = vm
PUIS:
Xi = vi
   .
   .
   .
.fill
;environnement et ses changements successifs par effets de bord;
.nofill
       REF (a1' a2' ... an')
.fill
;les ai' sont les representations conceptuelles des ai, c'est a dire
le resultat de leur meta-interpretation;
.nofill
          F1 --> F'1
          F2 --> F'2
             .
             .
             .
          Fa --> F'a
.fill
;representation conceptuelle de la definition de F. Ensemble non
ordonne de regles;
.nofill
(a1' a2' ... an')
<::>
F1
 .
 .
 .
(a1' a2' ... an')
<::>
Fa
.fill
;les arguments meta-evalues sont confrontes a chaque regle.
Si l'unification reussit, il s'imprime:
.break
ALIST: resultat.
.break
;chaque association est du type:
.nofill
(nom (i1 v1) (i2 v2) ... (in vn))
qui equivaut a:
((nomi1 = v1)(nomi2 = v2) ... (nomin = vn))
un cas particulier:
(nom (i f(i) B v(i)))
associe a tout nomf(i) pour i de 1 a B, v(i);
.fill
.page
.SKIP 25
.CENTER;APPENDICE 2
.CENTER;LISTING DU META-FILTREUR
.SKIP 25
.PAGE
.SKIP 25
.CENTER;APPENDICE 3
.CENTER;LISTING DU META-INTERPRETE
.SKIP 25
.PAGE
.SKIP 25
.CENTER;APPENDICE 4
.CENTER;REPRESENTATIONS CONCEPTUELLES
.CENTER;DE QUELQUES FONCTIONS LISP
.SKIP 25
.PAGE
X